Existing systems for controlling traffic of railroad vehicles are classified into “safety related systems” for securing safety in operation thereof and “non-safety related systems” for achieving various purposes independently thereof.
“Security systems” are systems for controlling traffic of trains such that the trains neither collide nor derail. Representative examples thereof include an automatic train control (ATC) system and an “interlock system”. Here, an “interlock system” means a system that controls traffic signals and switch stands (devices that switch a route of a train in a branch) to interlock with each other.
On the other hand, “non-safety related systems” mean systems not corresponding to the “safety related systems” among systems mainly required for operating railroads as a transportation system. A representative example thereof is a “traffic control system” that causes a train to travel or stop in accordance with a train diagram. Ticket examination facilities and the like are also examples thereof.
In a train traffic control system that controls traffic of trains while causing the traffic control system which is a non-safety related system and the interlock system which is a safety related system to function independently, it is necessary to form a traffic logic which do not cause “deadlock” in a traffic processes thereof. Here, the “deadlock” means a state in communication between the traffic control system and the interlock system in which the traffic processes of trains can no longer progress.
Therefore, a designer of traffic logic needs to verify in advance whether the “deadlock” can occur in the traffic processes that are sequentially performed in accordance with the traffic logic.
Regarding the “interlock system” as the “safety related system”, a method of automating verification of such an operation and saving energy is disclosed (Patent Literature 1).